\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $v$:ecl{-}trans{-}tuple\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$).
\-\\[0ex]ecl{-}trans{-}normal($v$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List). \+
\\[0ex]($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List). 
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); $L$; ${\it L'}$) $\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)(0,$L$)) $\Rightarrow$ False)
\\[0ex]$\Rightarrow$ (\=ecl{-}trans{-}state(reset{-}ecl{-}tuple($v$); ${\it L'}$)\+
\\[0ex]=
\\[0ex]ecl{-}trans{-}state($v$; ${\it L'}$)
\\[0ex]$\in$ ecl{-}trans{-}type(reset{-}ecl{-}tuple($v$))))
\-\-
\end{tabbing}